Skip to content

feat(lift-go): lift leading guard-panics into preconditions#1561

Merged
TSavo merged 1 commit into
mainfrom
feat/go-guard-precondition
May 27, 2026
Merged

feat(lift-go): lift leading guard-panics into preconditions#1561
TSavo merged 1 commit into
mainfrom
feat/go-guard-precondition

Conversation

@TSavo
Copy link
Copy Markdown
Owner

@TSavo TSavo commented May 27, 2026

The Go production lifter emitted pre = true for every function, so a consumer's defensive guard (if !P(args){panic}) never became a contract precondition — invisible at call sites. This brings Go to parity with Rust (lift_function_precondition) and C# (LiftMethodPrecondition).

  • Leading if !P{panic}pre = P == true; bare if cond{panic}cond == false.
  • Scans only leading guards, stops at the first non-guard, refuses to invent a precondition from an unliftable condition.
  • CID-neutral for existing kits: the Go self-contracts contractSetCid is unchanged (073e4010…); no go-kit function uses the guard pattern. Lifter tests pass.

Unblocks BZ-DETERMINISM-001: a consumer's canonical_byte_order precondition now lifts from idiomatic Go — the first of the lifter features needed to build the determinism reference species honestly (no mock).

🤖 Generated with Claude Code

Summary by CodeRabbit

  • Improvements
    • Improved safety requirement analysis by deriving preconditions from defensive guards within function bodies rather than using empty default conditions. The system now examines leading conditional statements for panic-triggering patterns and converts them into precise safety constraints, delivering more accurate and comprehensive function safety analysis without inventing unfounded constraints.

Review Change Stack

The Go production lifter emitted `pre = true` for every function — a
consumer's defensive guard (`if !P(args){panic}`) never became a contract
precondition, so it was invisible at call sites. This brings Go to parity
with the Rust (lift_function_precondition) and C# (LiftMethodPrecondition)
walkers: a leading `if !P{panic}` lifts to `pre = P == true`, a bare
`if cond{panic}` to `cond == false`.

Scans only leading guards, stops at the first non-guard statement, and
refuses to invent a precondition from an unliftable condition. CID-neutral
for existing kits (the Go self-contracts contractSetCid is unchanged —
073e4010…; no go-kit function uses the guard pattern). Lifter tests pass.

Unblocks the BZ-DETERMINISM-001 reference species: a consumer's
canonical-byte-order precondition now lifts from idiomatic Go.

Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
@coderabbitai
Copy link
Copy Markdown

coderabbitai Bot commented May 27, 2026

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info
⚙️ Run configuration

Configuration used: Organization UI

Review profile: CHILL

Plan: Pro

Run ID: e43eecaa-d79e-4d1a-954c-15b087347099

📥 Commits

Reviewing files that changed from the base of the PR and between e610dac and f6eb5f5.

📒 Files selected for processing (1)
  • implementations/go/provekit-lift-go/lift.go

Walkthrough

The PR enhances function precondition derivation in the lifter by extracting conditions from leading defensive panic guards. Instead of starting with an empty precondition conjunction, liftFunc now scans the function body for eligible if guards that contain only panic statements and converts those guard conditions into precondition atoms.

Changes

Guard-Based Precondition Derivation

Layer / File(s) Summary
Integration of guard precondition extraction into liftFunc
implementations/go/provekit-lift-go/lift.go
liftFunc changes from computing pre as an always-empty ir.And() to calling formulaValue(liftLeadingGuardPreconditions(...)), enabling defensive panic guards to contribute to the emitted precondition.
Guard scanning and precondition atom generation
implementations/go/provekit-lift-go/lift.go
New helper functions scan leading if statements for panic-only guards, validate eligibility (no init, no else, single panic body), and convert valid guards into precondition atoms expressing the required caller conditions to avoid panic (including negated-condition handling).

Estimated code review effort

🎯 2 (Simple) | ⏱️ ~8 minutes

Poem

🐰 A guard stands watch at function's door,
With panic statements to explore,
We lift each shield to preconditions bright,
Converting guards to logic right!
The lifter learns what callers must know—
No panics here will ever flow!

🚥 Pre-merge checks | ✅ 5
✅ Passed checks (5 passed)
Check name Status Explanation
Description Check ✅ Passed Check skipped - CodeRabbit’s high-level summary is enabled.
Title check ✅ Passed The title clearly and specifically describes the main change: lifting leading guard-panic patterns into preconditions in the Go lifter, which is the primary purpose of this PR.
Docstring Coverage ✅ Passed No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.
Linked Issues check ✅ Passed Check skipped because no linked issues were found for this pull request.
Out of Scope Changes check ✅ Passed Check skipped because no linked issues were found for this pull request.

✏️ Tip: You can configure your own custom pre-merge checks in the settings.

✨ Finishing Touches
📝 Generate docstrings
  • Create stacked PR
  • Commit on current branch
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch feat/go-guard-precondition

Warning

There were issues while running some tools. Please review the errors and either fix the tool's configuration or disable the tool if it's a critical failure.

🔧 golangci-lint (2.12.2)

level=error msg="[linters_context] typechecking error: pattern ./...: directory prefix . does not contain main module or its selected dependencies"


Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands and usage tips.

Copy link
Copy Markdown

@chatgpt-codex-connector chatgpt-codex-connector Bot left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

💡 Codex Review

Here are some automated review suggestions for this pull request.

Reviewed commit: f6eb5f5aab

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

  • Open a pull request for review
  • Mark a draft as ready
  • Comment "@codex review".

If Codex has suggestions, it will comment; otherwise it will react with 👍.

Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".

Comment on lines +412 to +413
ident, ok := call.Fun.(*ast.Ident)
return ok && ident.Name == "panic"
Copy link
Copy Markdown

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

P2 Badge Resolve panic before lifting a guard

When a package-level symbol or parameter named panic shadows the predeclared builtin (for example func F(panic func(string), x int) int { if x < 0 { panic("bad") }; return x }), this syntactic name check treats the callback call as an aborting guard and emits x >= 0 as a precondition even though the call may return normally. The rest of the lifter already resolves callees through types.Info and would not record a panics effect for this shadowed call, so the new precondition is inconsistent with the modeled body; check that the callee resolves to the builtin panic before lifting the guard.

Useful? React with 👍 / 👎.

@TSavo TSavo merged commit 108be23 into main May 27, 2026
16 of 18 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant